predicate ok (f) =
   forall x. pre (f) (x)

let f (x) = x
lemma l : ok (f)
